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: |
|---|---|---|---|
| maplet-singleton-heap | proved | all subs proved | mod-def, maplet, |
| maplet | proved | all subs proved | mod-def, maplet-def, |
| ext | proved | all subs proved | sela-def, selo-def, |
| true-elim | proved | all subs proved | modifysep-def, |
| mk-exists | proved | all subs proved | mk-def, |
| mapex-put-rw | proved | all subs proved | maplet-def, mod-def, |
| ex3-shiftw | proved | all subs proved | ex3, |
| at-unir-M02 | proved | all subs proved | sela-def, mk-def, |
| at-rw | proved | all subs proved | modifysep-def, maplet-def, |
| prop-true | proved | all subs proved | modifysep-def, |
| map-write-M02 | proved | all subs proved | maplet-def, mod-def, |
| write-del | proved | all subs proved | mod-def, |
| in-mk | proved | all subs proved | mk-def, |
| mapex-elim-01 | proved | all subs proved | maplet-def, |
| del | proved | all subs proved | mk-def, |
| map-put-rw | proved | all subs proved | maplet-def, mod-def, |
| mapex-in0 | proved | all subs proved | modifysep-def, |
| at-alloc-M01 | proved | all subs proved | selo-def, |
| at-write-M01 | proved | all subs proved | selo-def, mod-def, |
| prop-emp | proved | all subs proved | modifysep-def, |
| ex3-shiftw-inst | proved | all subs proved | ex3, |
| split-uni | proved | all subs proved | modifysep-def, |
| at-del-M01 | proved | all subs proved | selo-def, |
| ex3-shift-01 | proved | all subs proved | ex3, modifysep-def, |
| uni | proved | all subs proved | mk-def, |
| eq-objs-M01 | proved | all subs proved | maplet-def, |
| mapex-new | proved | all subs proved | modifysep-def, |
| apply | proved | all subs proved | mk-def, modifysep-def, |
| ex1-shift | proved | all subs proved | modifysep-def, |
| mapex-del | proved | all subs proved | modifysep-def, |
| map-same | proved | all subs proved | maplet-def, |
| at-rw-M01 | proved | all subs proved | maplet-def, selo-def, |
| at-unil-M01 | proved | all subs proved | selo-def, mk-def, |
| mapex-elim | proved | all subs proved | modifysep-def, maplet-def, |
| map-putrev | proved | all subs proved | modifysep-def, maplet-def, |
| write | proved | all subs proved | mod-def, mk-def, |
| at-eq | proved | all subs proved | maplet-def, sela-def, selo-def, |
| mapex-put-01 | proved | all subs proved | maplet-def, mod-def, |
| map-in0-02 | proved | all subs proved | maplet-def, |
| write-right | proved | all subs proved | mod-def, |
| eq-objs-M02 | proved | all subs proved | maplet-def, |
| ex3-03 | proved | all subs proved | ex3, |
| sep | proved | all subs proved | modifysep-def, |
| at-alloc-M02 | proved | all subs proved | sela-def, |
| at-mk-M01 | proved | all subs proved | selo-def, mk-def, |
| map-put-01 | proved | all subs proved | maplet-def, mod-def, |
| at-write-M02 | proved | all subs proved | sela-def, mod-def, |
| prop | proved | all subs proved | modifysep-def, |
| map-put | proved | all subs proved | modifysep-def, maplet-def, |
| map-null | proved | all subs proved | maplet-def, |
| at-del-M02 | proved | all subs proved | sela-def, |
| mapex | proved | all subs proved | ex3, maplet-def, |
| precise-map | proved | all subs proved | maplet-def, |
| mk-ext | proved | all subs proved | modifysep-def, |
| in-uni | proved | all subs proved | mk-def, |
| in-write | proved | all subs proved | mod-def, |
| emp | proved | all subs proved | mk-def, |
| ex2-shift | proved | all subs proved | modifysep-def, |
| map-write-M01 | proved | all subs proved | maplet-def, mod-def, |
| map-putex | proved | all subs proved | maplet-def, mod-def, |
| at-unil-M02 | proved | all subs proved | sela-def, mk-def, |
| at-rw0 | proved | all subs proved | modifysep-def, maplet-def, |
| prop-false | proved | all subs proved | modifysep-def, |
| at-rw-M02 | proved | all subs proved | maplet-def, sela-def, |
| map-del-01 | proved | all subs proved | sela-def, selo-def, maplet-def, |
| map-in | proved | all subs proved | modifysep-def, maplet-def, |
| map-in-01 | proved | all subs proved | maplet-def, |
| true-emp | proved | all subs proved | modifysep-def, |
| mapex-put | proved | all subs proved | maplet-def, modifysep-def, |
| ex3-shift | proved | all subs proved | ex3, |
| at-unir-M01 | proved | all subs proved | selo-def, mk-def, |
| size-write | proved | all subs proved | mod-def, |
| at-mk-M02 | proved | all subs proved | sela-def, mk-def, |
| map-del | proved | all subs proved | modifysep-def, maplet-def, |
| write-left | proved | all subs proved | mod-def, |
| map-in0 | proved | all subs proved | modifysep-def, maplet-def, |
| mapex-in | proved | all subs proved | modifysep-def, |
| disj | proved | all subs proved | mk-def, |
| mapex-and | proved | all subs proved | maplet-def, |
| prop-sep | proved | all subs proved | modifysep-def, |
| diff-write | proved | all subs proved | mod-def, |
| ex3 | axiom | ||
| selo-def | axiom | ||
| sela-def | axiom | ||
| mk-def | axiom | ||
| maplet-def | axiom | ||
| modifysep-def | axiom | ||
| mod-def | axiom |