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: |
|---|
| union-newref-01 | proved | all subs proved
| union-newref-02,
|
| union-newref | proved | all subs proved
| refs-def,
union-newref-02,
|
| union-init-03 | proved | all subs proved
| union-init,
|
| union-init-02 | proved | all subs proved
| union-init,
|
| union-newref-02 | proved | all subs proved
| union-in-01,
|
| union-init | proved | all subs proved
| union-at-right-02,
union-in,
union-init-01,
|
| mode-notin-02 | proved | all subs proved
| refs-def,
mode-notin-01,
|
| refs-equal | proved | all subs proved
| instore-inrefs-02,
refs-def,
refs-del,
refs-empty,
refs-empty-01,
|
| refs-equal-in | proved | all subs proved
| instore-inrefs-02,
refs-empty-01,
instore-inrefs,
|
| reftype-int-02 | proved | all subs proved
| reftypep,
reftype-int-01,
reftype-02,
|
| subset-is-union | proved | all subs proved
| union-at-right-01,
lookup-xtra,
union-at-left,
union-in,
union-rec,
union-empty,
union-subset,
|
| subset-size | proved | all subs proved
| instore-inrefs-02,
refs-notin,
refs-del,
instore-inrefs-01,
lookup-xtra,
refs-empty-01,
refs-put,
refs-empty,
|
| union-refs | proved | all subs proved
| union-in-01,
refs-def,
|
| mode-notin-01 | proved | all subs proved
| mode-notin,
union-at-right-02,
|
| reftype-int-01 | proved | all subs proved
| reftype-03,
|
| union-subset | proved | all subs proved
| union-at-right-01,
union-in,
|
| instore-inrefs-02 | proved | all subs proved
| refs-def,
refs-empty-01,
|
| union-init-01 | proved | all subs proved
| union-at-right-02,
union-in,
|
| union-in-01 | proved | all subs proved
| union-in,
|
| union-subset-left | proved | all subs proved
| instore-inrefs-01,
union-at-right-01,
union-at-left,
union-in,
|
| union-in-02 | proved | all subs proved
| refs-notin,
union-in,
|
| union-empty-01 | proved | all subs proved
| union-at-right-02,
union-in,
|
| union-at-right-03 | proved | all subs proved
| refs-notin,
union-at-right-02,
|
| eqex-tput | proved | all subs proved
| eqex,
eqex-ref,
eqex-trans,
eqex-sym,
|
| eqex-mode | proved | all subs proved
| eqex,
eqex-ref,
eqex-trans,
eqex-sym,
|
| classof-03 | proved | all subs proved
| classOf,
classof-06,
classof-02,
|
| union-in | proved | all subs proved
| union-at-left,
union-at-right-01,
union-def,
|
| reftype-03 | proved | all subs proved
| reftype-02,
reftype-jvmref,
reftypep,
|
| union-at-right-02 | proved | all subs proved
| lookup-xtra,
union-at-left,
union-at-right-01,
|
| refs-empty-01 | proved | all subs proved
| refs-notin,
lookup-xtra,
refs-empty,
|
| eqex-trans | proved | all subs proved
| eqex,
eqex-sym,
|
| classof-02 | proved | all subs proved
| classOf,
classof-06,
|
| exception-03 | proved | all subs proved
| exception-01,
exception,
|
| nouninit-mode-01 | proved | all subs proved
| nouninit-undone,
nouninit,
|
| nouninit-put-02 | proved | all subs proved
| nouninit-undone,
nouninit,
|
| onlymod-del | proved | all subs proved
| lookup-xtra,
onlymod-in,
onlyModified,
|
| onlymod-in-01 | proved | all subs proved
| onlymod-sym-01,
onlymod-in,
|
| onlymod-init | proved | all subs proved
| onlymod-init-01,
onlymod-sym-01,
onlymod-init-02,
|
| onlymod-length-01 | proved | all subs proved
| onlymod-length,
|
| onlymod-mode-01 | proved | all subs proved
| onlymod-mode,
|
| onlymod-put | proved | all subs proved
| onlymod-in,
onlyModified,
|
| onlymod-sym | proved | all subs proved
| onlymod-sym-01,
|
| reftype-int | proved | all subs proved
| reftype-put,
|
| union-at-right | proved | all subs proved
| union-at-right-01,
|
| classof-06 | proved | all subs proved
| classOf,
|
| eqex-ref | proved | all subs proved
| eqex,
|
| eqex-sym | proved | all subs proved
| eqex,
|
| exception-01 | proved | all subs proved
| exception,
|
| mode-notin | proved | all subs proved
| refs-def,
|
| nouninit-undone | proved | all subs proved
| nouninit,
|
| onlymod-init-01 | proved | all subs proved
| onlyModified,
|
| onlymod-init-02 | proved | all subs proved
| onlyModified,
|
| onlymod-length | proved | all subs proved
| lookup-xtra,
onlyModified,
|
| onlymod-mode | proved | all subs proved
| onlyModified,
|
| onlymod-in | proved | all subs proved
| onlyModified,
|
| onlymod-sym-01 | proved | all subs proved
| onlyModified,
|
| instore-inrefs | proved | all subs proved
| refs-def,
|
| reftype-jvmref | proved | all subs proved
| reftypep,
|
| reftype-put | proved | all subs proved
| reftypep,
|
| reftype-02 | proved | all subs proved
| reftypep,
|
| refs-del | proved | all subs proved
| refs-def,
|
| refs-put | proved | all subs proved
| refs-def,
|
| refs-empty | proved | all subs proved
| refs-def,
|
| union-def | proved | all subs proved
| union-rec,
union-empty,
|
| refs-notin | proved | all subs proved
| refs-def,
|
| instore-inrefs-01 | proved | all subs proved
| refs-def,
|
| union-at-right-01 | proved | all subs proved
| union-rec,
lookup-xtra,
union-empty,
|
| union-at-left | proved | all subs proved
| union-rec,
union-empty,
|
| union-rec-rew | proved | all subs proved
| union-rec,
|
| union-keys | proved | all subs proved
| union-rec,
union-empty,
|
| uninit-uninit | proved | all subs proved
| uninit,
|
| uninit-rec | proved | all subs proved
| uninit,
|
| uninit-one | proved | all subs proved
| uninit,
|
| uninit-empty | proved | all subs proved
| uninit,
|
| reftype-out | proved | all subs proved
| reftypep,
|
| reftype-mode | proved | all subs proved
| reftypep,
|
| reftype-04 | proved | all subs proved
| reftypep,
|
| reftype-01 | proved | all subs proved
| reftypep,
|
| onlymod-type | proved | all subs proved
| lookup-xtra,
onlyModified,
|
| onlymod-shift | proved | all subs proved
| onlyModified,
|
| onlymod-same | proved | all subs proved
| onlyModified,
|
| onlymod-put-01 | proved | all subs proved
| onlyModified,
|
| onlymod-other | proved | all subs proved
| onlyModified,
|
| nouninit-put-statfield | proved | all subs proved
| nouninit,
|
| nouninit-put-03 | proved | all subs proved
| nouninit,
|
| nouninit-put-01 | proved | all subs proved
| nouninit,
|
| nouninit-put | proved | all subs proved
| nouninit,
|
| nouninit-mode | proved | all subs proved
| nouninit,
|
| nouninit-empty | proved | all subs proved
| nouninit,
|
| newref-same | proved | all subs proved
| refs-def,
|
| initerror-one | proved | all subs proved
| initerror,
|
| initdone-rec | proved | all subs proved
| initdone-def,
|
| initdone-one | proved | all subs proved
| initdone-def,
|
| initdone-empty | proved | all subs proved
| initdone-def,
|
| init-set | proved | all subs proved
| init,
|
| init-one | proved | all subs proved
| init,
|
| exception-02 | proved | all subs proved
| exception,
|
| eqmode-length | proved | all subs proved
| equalXmode,
|
| eqmode-01 | proved | all subs proved
| equalXmode,
|
| eqmode | proved | all subs proved
| equalXmode,
|
| eqex-at | proved | all subs proved
| eqex,
|
| eq-mod | proved | all subs proved
| equalXmode,
exception,
|
| classof-07 | proved | all subs proved
| classOf,
|
| classof-05 | proved | all subs proved
| classOf,
|
| classof-04 | proved | all subs proved
| classOf,
|
| classof-01 | proved | all subs proved
| classOf,
|
| classof | proved | all subs proved
| classOf,
|
| uninit | axiom | | |
| union-empty | axiom | | |
| union-rec | axiom | | |
| reftypep | axiom | | |
| onlyModified | axiom | | |
| lookup-xtra | axiom | | |
| nouninit | axiom | | |
| refs-def | axiom | | |
| initerror | axiom | | |
| initdone-def | axiom | | |
| init | axiom | | |
| eqex | axiom | | |
| exception | axiom | | |
| equalXmode | axiom | | |
| classOf | axiom | | |