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: |
|---|---|---|---|
| alloc | proved | all subs proved | owned-emp, alloc-p, |
| alloc-p | proved | all subs proved | owned-r, owned-P, rely, owned, compact-local, switch-ownership, lift-mapex, |
| write-unknown | proved | all subs proved | write-unknown-p, |
| write-unknown-p | proved | all subs proved | write-known-p, ex-shift-o-p, |
| switch-ownership | proved | all subs proved | owned-P, rely, owned, |
| compact-local | proved | all subs proved | owned-P, owned-r, owned, |
| guar-refl | proved | all subs proved | rely-refl, guar, |
| propagate | proved | all subs proved | owned-r, rely, |
| write-known | proved | all subs proved | write-known-p, |
| ex-shift-o-p | proved | all subs proved | owned, |
| rely-refl | proved | all subs proved | rely, |
| lift-mapex | proved | all subs proved | owned, |
| owned-emp | proved | all subs proved | owned, |
| owned-r | proved | all subs proved | owned, |
| owned-P | proved | all subs proved | owned, |
| write-known-p | proved | all subs proved | owned, |
| guar-rely | proved | all subs proved | guar, |
| lift-map | proved | all subs proved | owned, |
| rely-trans | proved | all subs proved | rely, |
| ex-shift-o | proved | all subs proved | owned, |
| guar | axiom | ||
| rely | axiom | ||
| owned | axiom |