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: |
|---|
| hasSharing-put-index-refval | proved | all subs proved
| fits-storekeys-rec,
hasSharing-def-better,
hasSharing-self,
disjoint-def-fits,
fits-storekeys-empty,
fits-rec,
fits-null,
fits-append,
fits-put-other,
hasSharing-def,
|
| hasSharing-addobj-same | proved | all subs proved
| fits-storekeys-empty,
fits-in,
fits-storekeys-one,
disjoint-def-fits,
hasSharing-def-better,
hasSharing-list-def,
fits-null,
fits-in-01,
fits-subset-01,
fits-rec,
hasSharing-def,
|
| addarray-disjoint-nosharing-01 | proved | all subs proved
| disjoint-def-fits,
fits-in-01,
fits-null,
hasSharing-def-better,
hasSharing-list-def,
fits-storekeys-empty,
fits-in,
fits-subset-01,
fits-rec,
hasSharing-def,
|
| addarray-disjoint-nosharing | proved | all subs proved
| fits-null,
disjoint-def-fits,
hasSharing-def-better,
hasSharing-list-def,
fits-storekeys-empty,
fits-in,
fits-subset-01,
fits-rec,
hasSharing-def,
|
| hasSharing-self | proved | all subs proved
| fits-storekeys-empty,
hasSharing-def-better,
|
| disjoint-def-fits | proved | all subs proved
| ex-validrefs-fits,
ex-fits-validrefs,
disjoint-def,
|
| disjoint-nopath-both | proved | all subs proved
| disjoint-def-pathex,
disjoint-pathex-forward-both,
disjoint-nopathex-same,
|
| fits-pathex-01 | proved | all subs proved
| fits-pathex,
|
| hasSharing-addarray | proved | all subs proved
| hasSharing-subset,
|
| hasSharing-different-disjoint | proved | all subs proved
| hasSharing-dd-help,
disjoint-def,
|
| nosharing-nocycle | proved | all subs proved
| hassharing-validrefs-dups,
|
| put-switch-primval-field-field | proved | all subs proved
| fits-no-reftype-01,
fits-no-refval-01,
|
| put-switch-primval-field-index | proved | all subs proved
| fits-no-reftype,
fits-append,
at-put-prim,
fits-no-reftype-01,
fits-storekeys-one,
fits-no-refval-01,
|
| put-switch-primval-index-field | proved | all subs proved
| fits-no-reftype,
fits-append,
at-put-prim,
fits-no-reftype-01,
fits-storekeys-one,
fits-no-refval-01,
|
| put-switch-primval-index-index | proved | all subs proved
| fits-storekeys-one,
fits-append,
at-put-prim,
fits-no-refval-01,
|
| ex-validrefs-fits | proved | all subs proved
| ex-validrefs-fits-stronger,
|
| disjoint-pathex-forward-both | proved | all subs proved
| disjoint-nopathex-same,
disjoint-symmetric,
disjoint-pathex-forward,
|
| fits-pathex | proved | all subs proved
| ex-fits-validrefs,
|
| hasSharing-subset | proved | all subs proved
| fits-in,
fits-subset,
hasSharing-def,
|
| fits-in-01 | proved | all subs proved
| fits-storekeys-empty,
fits-in,
|
| fits-subset-01 | proved | all subs proved
| fits-superset,
fits-subset,
|
| hasSharing-dd-help | proved | all subs proved
| hasSharing-def,
ex-validrefs-fits-stronger,
|
| hasSharing-def-better | proved | all subs proved
| fits-append,
fits-storekeys-empty,
hasSharing-def,
|
| hassharing-validrefs-dups | proved | all subs proved
| fits-storekeys-rec,
fits-append,
hasSharing-def,
ex-validrefs-fits-stronger,
|
| fits-no-reftype-01 | proved | all subs proved
| fits-null,
fits-storekeys-empty,
fits-storekeys-rec,
fits-no-reftype,
|
| fits-no-refval-01 | proved | all subs proved
| fits-no-refval,
|
| unchanged-lookup-list-generic | proved | all subs proved
| unchanged-fits,
fits-storekeys-rec,
fits-storekeys-one,
fits-null,
fits-storekeys-empty,
|
| sharing-twopaths | proved | all subs proved
| fits-append,
ex-validrefs-fits-stronger,
hasSharing-def,
|
| sharing-pathex-field-self-01 | proved | all subs proved
| fits-append,
ex-validrefs-fits-stronger,
fits-storekeys-one,
fits-storekeys-rec,
hasSharing-def,
|
| sharing-pathex-field-self | proved | all subs proved
| fits-append,
ex-validrefs-fits-stronger,
fits-storekeys-one,
fits-storekeys-rec,
hasSharing-def,
|
| hasSharing-put-statfield | proved | all subs proved
| fits-storekeys-rec,
lookup-statfield,
fits-put-statfield,
hasSharing-def,
|
| hasSharing-put-shortval | proved | all subs proved
| fits-put-short-01,
fits-put-short-02,
fits-put-short,
hasSharing-def,
|
| hasSharing-put-byteval-01 | proved | all subs proved
| fits-put-05-stronger,
fits-put-03,
fits-put-04,
hasSharing-def,
|
| hasSharing-put-byteval | proved | all subs proved
| fits-put-stronger,
fits-put-02-stronger,
fits-put,
fits-put-01,
hasSharing-def,
|
| disjoint-subset-01 | proved | all subs proved
| disjoint-subset,
|
| disjoint-forward-field-02 | proved | all subs proved
| disjoint-forward-field,
|
| disjoint-forward-array-01 | proved | all subs proved
| disjoint-forward-array,
|
| unchanged-fits | proved | all subs proved
| fits-null,
fits-rec,
fits-storekeys-empty,
|
| fits-put-statfield | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-put-short | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-one,
fits-storekeys-empty,
|
| fits-put-short-02 | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-put-short-01 | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-put-other | proved | all subs proved
| fits-rec,
fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-put-04 | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-put-03 | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-one,
fits-storekeys-empty,
|
| fits-put-05-stronger | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-put-01 | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-empty,
fits-null,
|
| fits-append | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-one,
fits-storekeys-empty,
|
| fits-superset | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-no-refval | proved | all subs proved
| fits-null,
fits-storekeys-rec,
|
| fits-no-reftype | proved | all subs proved
| fits-null,
fits-storekeys-empty,
fits-storekeys-rec,
|
| ex-validrefs-fits-stronger | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| disjoint-subset | proved | all subs proved
| disjoint-def-pathex,
|
| disjoint-pathex-forward | proved | all subs proved
| disjoint-nopathex,
disjoint-def-pathex,
|
| disjoint-nopathex-same | proved | all subs proved
| disjoint-def-pathex,
|
| disjoint-forward-field | proved | all subs proved
| disjoint-def-pathex,
|
| disjoint-forward-array | proved | all subs proved
| disjoint-def-pathex,
|
| ex-fits-validrefs | proved | all subs proved
| fits-storekeys-empty,
ex-fits-validrefs-stronger,
|
| fits-in | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-one,
|
| fits-put-02 | proved | all subs proved
| fits-null,
fits-storekeys-rec,
fits-storekeys-empty,
|
| getbar-onlyModified | proved | all subs proved
| onlymodified-def,
getbar-onlyModified-all,
|
| hasSharing-dups-array | proved | all subs proved
| fits-storekeys-one,
hasSharing-def,
|
| hasSharing-dups-object | proved | all subs proved
| fits-storekeys-one,
hasSharing-def,
|
| hasSharing-pathex | proved | all subs proved
| hasSharing-array-forward,
hasSharing-object-rec,
|
| hasSharing-putbar | proved | all subs proved
| fits-put-02-stronger,
fits-put-stronger,
hasSharing-def,
|
| hassharing-bytearray | proved | all subs proved
| fits-rec,
hasSharing-def,
|
| disjoint-nopathex | proved | all subs proved
| disjoint-def,
|
| disjoint-symmetric | proved | all subs proved
| disjoint-def,
|
| disjoint-def-pathex | proved | all subs proved
| disjoint-def,
|
| ex-fits-validrefs-stronger | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-empty,
|
| getbar-onlyModified-all | proved | all subs proved
| onlymodified-def,
|
| hasSharing-array-forward | proved | all subs proved
| fits-storekeys-rec,
hasSharing-def,
|
| hasSharing-object-rec | proved | all subs proved
| fits-storekeys-rec,
hasSharing-def,
|
| fits-put | proved | all subs proved
| fits-storekeys-empty,
fits-storekeys-rec,
|
| lookup-statfield | proved | all subs proved
| fits-storekeys-rec,
|
| fits-put-02-stronger | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-empty,
|
| fits-put-stronger | proved | all subs proved
| fits-storekeys-empty,
fits-storekeys-rec,
|
| fits-subset | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-empty,
|
| at-put-prim | proved | all subs proved
| fits-storekeys-empty,
fits-storekeys-rec,
|
| fits-rec | proved | all subs proved
| fits-storekeys-rec,
|
| fits-storekeys-one | proved | all subs proved
| fits-storekeys-empty,
fits-storekeys-rec,
|
| fits-null | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-empty,
|
| unchanged-put-nosharing | proved | all subs proved
| disjoint-def,
|
| putbar-classfield-onlymod | proved | all subs proved
| onlymodified-def,
|
| putBar-onlyMod | proved | all subs proved
| onlymodified-def,
|
| nosharing-forward | proved | all subs proved
| fits-storekeys-rec,
hasSharing-def,
|
| hassharing-one | proved | all subs proved
| hasSharing-list-def,
|
| hasSharing-rec | proved | all subs proved
| hasSharing-list-def,
|
| fits-put-05 | proved | all subs proved
| fits-storekeys-rec,
fits-storekeys-empty,
|
| disjoint-one | proved | all subs proved
| disjoint-def,
|
| disjoint-nojunk-newref-subset-01 | proved | all subs proved
| disjoint-def,
|
| disjoint-nojunk-newref-subset | proved | all subs proved
| disjoint-def,
|
| disjoint-newref-02 | proved | all subs proved
| disjoint-def,
|
| disjoint-newref-01 | proved | all subs proved
| disjoint-def,
|
| disjoint-newref | proved | all subs proved
| disjoint-def,
|
| onlymodified-def | axiom | | |
| disjoint-def | axiom | | |
| fits-storekeys-rec | axiom | | |
| hasSharing-def | axiom | | |
| fits-storekeys-empty | axiom | | |
| hasSharing-list-def | axiom | | |